$\forall$${\it es}$:event\_system\{i:l\}, $d$,$b$,$a$,$c$:es{-}E(${\it es}$).
\\[0ex]es{-}le(${\it es}$; $a$; $b$)
\\[0ex]$\Rightarrow$ es{-}le(${\it es}$; $c$; $d$)
\\[0ex]$\Rightarrow$ ([$a$, $b$] = [$c$, $d$] $\in$ (es{-}E(${\it es}$) List))
\\[0ex]$\Rightarrow$ guard((($a$ = $c$) $\wedge$ ($b$ = $d$)))